FDL - Nuprl Lemma : assert-es-eq-E

Nuprl Lemma : assert-es-eq-E

the_es:ES, e, e':E. e = e'

e = e'

Definitions ES, E, e = e', Prop, b, eqof(d), x:A. B(x), t T, P Q, P & Q, P Q, P Q

Lemmas eqof wf, assert wf, deq property, iff functionality wrt iff, event system wf